<,+> == <, x,y. (x = y), x,y. x z y, x,y. x+y, 0, x.x> 

latex

Up	groups 1
Wellformedness Lemmas	nat add mon wf, nat add mon wf2
Definitions	, (i = j), i z j